FDL - Nuprl Lemma : vartype-es-state-sub

Nuprl Lemma : vartype-es-state-sub

es:ES, i:Id, ds1, ds2:x:Id fp

Type.
ds2

ds1

(

x:Id. vartype(i;x)

ds1(x)?Top)

state@i

State(ds2)

Definitions state@i, State(ds), f g, a:A fp B(a), ES, P Q, x. t(x), IdDeq, f(x)?z, Top, vartype(i;x), x:A. B(x), t T, Id

Lemmas subtype-fpf-cap-top, Id wf, subtype rel self, top wf, id-deq wf, fpf-cap wf, es-vartype wf, subtype rel dep function, event system wf, fpf wf, fpf-sub wf